@$i$ $x$ has type $T$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$e$@$i$. ($x$ when $e$) $\in$ $T$ \& ($x$ after $e$) $\in$ $T$